Inference at * 1 1 1 0 
Iof proof for Lemma l before antisymmetry:



1. T : Type
2. l : T List
3. x : T
4. y : T
5. no_repeats(T;l)
6. [x; y]  l
7. [y; x]  l
  [x; x]  [x; y; x] 

latex

 by PERMUTE{1:n, 2:n, 2:n, 3:n, 4:n, 5:n} 

latex

 1: .....wf..... NILNIL

 1:   T  Type
 2: .....wf..... NILNIL

 2:   x  T
 3: .....wf..... NILNIL

 3:   [x]  (T List)
 4: .....wf..... NILNIL

 4:   [y; x]  (T List)
 5: 

 5:   (x = x & [x]  [y; x])  [x; x]  [y; x]
 .

Definitions	t  T, x:A  B(x), f(a), x:AB(x), s = t, P  Q, [], [car / cdr], L1  L2, no_repeats(T;l), type List, Type, P  Q, x:A. B(x), P  Q, P & Q, P  Q
Lemmas	cons sublist cons